T:Type, c:T, i:Id. AtomFree(Type;T)  constR{x:ut2}(T; c; i)  Realizer 

latex

Definitions	Id, P  Q, constR{$x:ut2}(T; c; i), x:A. B(x), "$x", t  T, Prop
Lemmas	atom-free wf, Rframe wf, Rlist wf, Knd wf, Id wf, Rinit wf, es realizer wf